/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;

import salvo.jesus.graph.DirectedGraph;
import salvo.jesus.graph.DirectedGraphImpl;
import salvo.jesus.graph.Vertex;
import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.ArrowMultExpr;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.ComprehensionExpr;
import alloy.ast.ElemFormula;
import alloy.ast.EmptySetExpr;
import alloy.ast.Expr;
import alloy.ast.ExprCastIntExpr;
import alloy.ast.HasType;
import alloy.ast.IdentityExpr;
import alloy.ast.IfThenElseExpr;
import alloy.ast.IntExprCastExpr;
import alloy.ast.InvocationExpr;
import alloy.ast.InvocationFormula;
import alloy.ast.LetFormula;
import alloy.ast.LetImpl;
import alloy.ast.ModuleInfo;
import alloy.ast.MultiplicityExpr;
import alloy.ast.QuantifiedFormula;
import alloy.ast.SetMultExpr;
import alloy.ast.Signature;
import alloy.ast.SumExpr;
import alloy.ast.SumIntExpr;
import alloy.ast.UnaryExpr;
import alloy.ast.UnaryExprOp;
import alloy.ast.UniversalExpr;
import alloy.ast.VariableExpr;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.type.UnionType;
import alloy.util.Dbg;

/**
 * This visitor resolves the ovverloaded types computed by ExprTypeCheckVisitor.
 * The visitor operates in a top-down fashion.  In other words, it uses the
 * information about the resolution of a parent expression to compute the
 * resolution of a child expression and to detect inessential unions.
 **/
class OverloadingResolutionVisitor extends ASTDepthFirstVisitor {

    /** current ModuleInfo **/
    private ModuleInfo _moduleInfo;

     /** the LocalScope enclosing the expressions */
    private LocalScope _localScope;

    private TypeErrorReporter _err;

    /**
     * @param moduleInfo_ the current module info
     * @param localScope_ the current local scope
     * @param err_ the error reporter to be used
     **/
    public OverloadingResolutionVisitor(ModuleInfo moduleInfo_, 
					LocalScope localScope_,
					TypeErrorReporter err_) {
	_moduleInfo = moduleInfo_;
	_localScope = localScope_;
	_err = err_;
    }

    public TypeErrorReporter getReporter() {
	return _err;
    }

    //*************//
    // EXPRESSIONS //
    //*************//

    /**
     * If type[child] & type[union] is empty, an inessential union error is reported 
     * (unless type[child] or type[union]] has size 0).  Otherwise, child is typed to be 
     * type[child] & type[union]
     * @param union Expr whose type is the union of the types of its subexpressions
     * @param childDescStr String describing the child in error messages (usually "left"
     * or "right")
     * @param child Expr that is either a left or a right child of union
     * EFFECTS: child's type is set to type[child] & type[union]   
     * 
     **/
    private void _unionResolveChild(Expr union, String childDescStr, Expr child) {

	UnionType childType = child.getType();
	UnionType unionType = union.getType();
	UnionType resolvedType = childType.intersect(unionType);

	if ((unionType.size() > 0) && (childType.size() > 0) && (resolvedType.isEmpty()))
	    _err.semantic("inessential union (" + childDescStr.toLowerCase() + " expression redundant)\n" +
			  TypeErrorReporter.format((Expr)union) + "\n" +
			  TypeErrorReporter.format(childDescStr, (HasType) child), union);
	    
	child.setType(resolvedType);
    }
    
   

    /**
     * @return a UnionType ut with a single RelationType rt that consists of 
     * BasicTypes from the supplied in BasicTypes list, starting at index start 
     * and ending at index end-1.  If the given
     * indices are out of range of basicTypes, a runtime exception is thrown.
     **/
    private static UnionType _makeUT(List basicTypes, int start, int end) {
	return new UnionType(new RelationType(basicTypes.subList(start,end)));
    }

    
    /**
     * @param parentType UnionType of left and right's parent expression
     * @param left left subexpression of a product expression
     * @param right right subexpression of a product expression
     * EFFECTS:  let leftType = type[left] and rightType = type[right].
     * This method sets the type of left child to leftType' and type of right child to 
     * rightType' where leftType' = {r1 | r1 in leftType and there exists r2 in rightType
     * such that r1->r2 in parentType} and rightType' = {r2 | r2 in rightType and 
     * there exists r1 in leftType such that r1->r2 in parentType}.   
     * 
     **/
    private void _differenceResolveChildren(UnionType parentType, HasType left, HasType right) {

       
	UnionType rightType = right.getType();
	UnionType resolvedType = parentType.intersect(rightType);

	if ((parentType.size() > 0) && (resolvedType.size() > 0) && (resolvedType.isEmpty()))
	    _err.semantic("inessential difference (right expression redundant)\n" +
			  TypeErrorReporter.format((Expr)right.getParent()) + "\n" +
			  TypeErrorReporter.format("Right", right), (Expr)right.getParent());
	    
	left.setType(parentType);
	right.setType(resolvedType);
    }
    
    /**
     * @param parentType UnionType of left and right's parent expression
     * @param left left subexpression of a product expression
     * @param right right subexpression of a product expression
     * EFFECTS:  let leftType = type[left] and rightType = type[right].
     * This method sets the type of left child to leftType' and type of right child to 
     * rightType' where leftType' = {r1 | r1 in leftType and there exists r2 in rightType
     * such that r1->r2 in parentType} and rightType' = {r2 | r2 in rightType and 
     * there exists r1 in leftType such that r1->r2 in parentType}.  
     **/
    private static void _productResolveChildren(UnionType parentType, 
						HasType left, HasType right) {
	UnionType leftType = new UnionType();
	UnionType rightType = new UnionType();
	
	for (Iterator leftIter = left.getType().getTypeIter(); leftIter.hasNext(); ) {
	    
	    RelationType lrt = (RelationType) leftIter.next();
	    
	    for (Iterator rightIter = right.getType().getTypeIter(); rightIter.hasNext();) {
		
		RelationType rrt = (RelationType) rightIter.next();
		if ((lrt.isEmpty() == rrt.isEmpty()) && 
		    parentType.hasArity(lrt.arity() + rrt.arity())) {

		    UnionType contribution = 
			parentType.intersect(new UnionType(lrt.product(rrt)));
		    
		    for (Iterator cIter = contribution.getTypeIter(); cIter.hasNext();) {
			RelationType crt = (RelationType) cIter.next();
			if (crt.isEmpty()) { continue; }
			List bts = crt.getBasicTypes();
			leftType = leftType.union(_makeUT(bts,0,lrt.arity()));
			rightType = rightType.union(_makeUT(bts,lrt.arity(), bts.size()));
						  
		    }
		}
	    }
	}
	
	left.setType(leftType);
	right.setType(rightType);
    }

    /**
     * @param parentType UnionType of left and right's parent expression
     * @param left left subexpression of a join expression
     * @param right right subexpression of a join expression
     * EFFECTS:  let leftType = type[left] and rightType = type[right].
     * This method sets the type of left child to leftType' and type of right child to 
     * rightType' where leftType' = {r1 | r1 in leftType and there exists r2 in rightType
     * such that r1.r2 in parentType} and rightType' = {r2 | r2 in rightType and 
     * there exists r1 in leftType such that r1.r2 in parentType}.  
     **/
    private static void _joinResolveChildren(UnionType parentType, Expr left, Expr right) {
	UnionType leftType = new UnionType();
	UnionType rightType = new UnionType();
	/*
	System.out.println("---------------------------");
	System.out.println("left: " + left + " " + left.getType());
	System.out.println("right: " + right + " " + right.getType());
	*/
	
	for (Iterator leftIter = left.getType().getTypeIter(); leftIter.hasNext(); ) {
	    RelationType lrt = (RelationType) leftIter.next();
	    for (Iterator rightIter = right.getType().getTypeIter(); rightIter.hasNext(); ) {
		RelationType rrt =  (RelationType) rightIter.next();

		if (parentType.hasArity(lrt.arity() + rrt.arity() - 2)) {

		    BasicType joinType = 
			lrt.getBasicTypeAt(lrt.arity()-1).intersect(rrt.getBasicTypeAt(0));

		    if (joinType.isEmpty()) { continue; }

		    UnionType contribution = 
			parentType.intersect(new UnionType(lrt.join(rrt)));
		    
		    for (Iterator cIter = contribution.getTypeIter(); cIter.hasNext();) {
			RelationType crt = (RelationType) cIter.next();
			if (crt.isEmpty()) { continue; }
			List bts = new LinkedList(crt.getBasicTypes());
			bts.add(lrt.arity()-1, joinType);
			leftType = leftType.union(_makeUT(bts,0,lrt.arity()));
			rightType = rightType.union(_makeUT(bts,lrt.arity()-1, bts.size()));
			
		    }
		    
		}
	    }
	}
	/*
	System.out.println("left: " + left + " " + leftType);
	System.out.println("right: " + right + " " + rightType);
	*/
	
	left.setType(leftType);
	right.setType(rightType);
    }

    
    /**
     * @param parentType UnionType of left and right's parent expression
     * @param left left subexpression of a domain restriction expression
     * @param right right subexpression of a domain restriction expression
     * EFFECTS:  let leftType = type[left] and rightType = type[right].
     * This method sets the type of left child to leftType' and type of right child to 
     * rightType' where leftType' = {r1 | r1 in leftType and there exists r2 in rightType
     * such that r1<:r2 in parentType} and rightType' = {r2 | r2 in rightType and 
     * there exists r1 in leftType such that r1<:r2 in parentType}.  
     **/
    private static void _domainRestrictResolveChildren(UnionType parentType, 
						       Expr left, Expr right) {
	UnionType leftType = new UnionType();
	UnionType rightType = new UnionType();
	
	for (Iterator leftIter = left.getType().getTypeIter(); leftIter.hasNext(); ) {
	    RelationType lrt = (RelationType) leftIter.next();
	    if (lrt.arity() != 1) { continue ;}
	    for (Iterator rightIter = right.getType().getTypeIter(); rightIter.hasNext();) {
		RelationType rrt = (RelationType) rightIter.next();
		if (parentType.hasArity(rrt.arity())) {
		    RelationType restricted = 
			rrt.columnRestrict(lrt.getBasicTypeAt(0), 0);
		    
		    if (restricted.isEmpty()) {continue;}
		    
		    UnionType contribution = 
			parentType.intersect(new UnionType(restricted));
		    
		    for (Iterator cIter = contribution.getTypeIter(); cIter.hasNext();) {
			List bts = ((RelationType) cIter.next()).getBasicTypes();
			leftType = leftType.union(_makeUT(bts, 0, 1));
			rightType = rightType.union(_makeUT(bts, 0, bts.size()));
		    }
		}
	    }
	    
	}
	
	left.setType(leftType);
	right.setType(rightType);
    }

    
    /**
     * @param parentType UnionType of left and right's parent expression
     * @param left left subexpression of a range restriction expression
     * @param right right subexpression of a range restriction expression
     * EFFECTS:  let leftType = type[left] and rightType = type[right].
     * This method sets the type of left child to leftType' and type of right child to 
     * rightType' where leftType' = {r1 | r1 in leftType and there exists r2 in rightType
     * such that r1:>r2 in parentType} and rightType' = {r2 | r2 in rightType and 
     * there exists r1 in leftType such that r1:>r2 in parentType}.  
     **/
    private static void _rangeRestrictResolveChildren(UnionType parentType, 
						      Expr left, Expr right) {
	UnionType leftType = new UnionType();
	UnionType rightType = new UnionType();
	
	for (Iterator rightIter = right.getType().getTypeIter(); rightIter.hasNext(); ) {
	    RelationType rrt = (RelationType) rightIter.next();
	    if (rrt.arity() != 1) { continue; }
	    for (Iterator leftIter = left.getType().getTypeIter(); leftIter.hasNext(); ) {
		RelationType lrt = (RelationType) leftIter.next();
		if (parentType.hasArity(lrt.arity())) {
		    RelationType restricted = 
			lrt.columnRestrict(rrt.getBasicTypeAt(0),lrt.arity()-1);
		    
		    if (restricted.isEmpty()) { continue; }

		    UnionType contribution = 
			parentType.intersect(new UnionType(restricted));
		    
		    for (Iterator cIter = contribution.getTypeIter(); cIter.hasNext();){
			List bts = ((RelationType) cIter.next()).getBasicTypes();
			leftType = leftType.union(_makeUT(bts,0,bts.size()));
			rightType = rightType.union(_makeUT(bts,bts.size()-1, bts.size()));
		    }
		}
	    }
	    
	}
	
	left.setType(leftType);
	right.setType(rightType);
    }


    /**
     * resolve overloadings for binary expressions
     * @param binaryExpr_ the expression
     */
    public void visit(BinaryExpr binaryExpr_) {

	Expr left = binaryExpr_.getLeft();
	Expr right = binaryExpr_.getRight();
	
	UnionType binType = binaryExpr_.getType();
	//System.out.println(binaryExpr_.toString() + ": " + binType.toString());
	//System.out.println(left.toString() + " computed " + left.getType().toString());
	//System.out.println(right.toString() + " computed " + right.getType().toString());
	
	// the types of left and
	// right child are set to their essential contribution to the
	// type of the binary expression (i.e. left and right
	// types contain only those RelationTypes that contribute to binType)
		 
	BinaryExprOp op = binaryExpr_.getOp();
	
	// for + and ++, leftType' = leftType & binType
	// and rightType' = rightType & binType
	if (op.equals(BinaryExprOp.UNION) ||
	    op.equals(BinaryExprOp.RELATIONALOVERRIDE)) {
	    // first, reduce types of left and right to their essential contribution . . .
	    _unionResolveChild(binaryExpr_, "Left", left);
	    _unionResolveChild(binaryExpr_, "Right", right);
	    // then, if this is a relational override, make sure that
	    // the essential left and right types are override-compatible
	    if (op.equals(BinaryExprOp.RELATIONALOVERRIDE) &&
		(!left.getType().isEmpty()) && (!right.getType().isEmpty()) &&
		(!right.getType().canOverride(left.getType()))) {
		_err.type("relevant types incompatible for relational override", 
			  binaryExpr_);
		
	    }
	    
	}
	
	// for -, leftType' = binType and rightType' = binType & rightType
	else if (op.equals(BinaryExprOp.DIFF)) {
	    //System.out.println(binaryExpr_.toString() + ": " + binType.toString());
	    //System.out.println(left.toString() + " computed " + left.getType().toString());
	    //System.out.println(right.toString() + " computed " + right.getType().toString());
	    //left.setType(binType);
	    //right.setType(binType.intersect(right.getType()));
	    _differenceResolveChildren(binType, left, right);
	    //System.out.println(left.toString() + " resolved " + left.getType().toString());
	    //System.out.println(right.toString() + " resolved " + right.getType().toString());

	}
	
	// for &, leftType' = binType & leftType and rightType' = binType & rightType
	else if (op.equals(BinaryExprOp.INTERSECT)) {
	    left.setType(binType.intersect(left.getType()));
	    right.setType(binType.intersect(right.getType()));
	}
	
	// for ->, leftType' = {r1 | r1 in leftType and there exists r2 in rightType
	// such that r1->r2 in binType} and rightType' = {r2 | r2 in rightType and 
	// there exists r1 in leftType such that r1->r2 in binType}
	else if (op.equals(BinaryExprOp.RELATION)) {
	    _productResolveChildren(binType, left, right);
	}
	
	// for join, leftType' = {r1 | r1 in leftType and there exists r2 in rightType
	// such that r1.r2 in binType} and rightType' = {r2 | r2 in rightType and 
	// there exists r1 in leftType such that r1.r2 in binType}
	else if (op.equals(BinaryExprOp.JOIN_DOT) ||
	        op.equals(BinaryExprOp.JOIN_DOUBLECOLON) ||
	        op.equals(BinaryExprOp.JOIN_SQBRACKETS)) {
	    _joinResolveChildren(binType, left, right);
	}
	
	else if (op.equals(BinaryExprOp.DOMAINRESTRICT)) {
	    _domainRestrictResolveChildren(binType, left, right);
	}
	
	else if (op.equals(BinaryExprOp.RANGERESTRICT)) {
	    _rangeRestrictResolveChildren(binType, left, right);
	}

	//System.out.println(left.toString() + " resolved " + left.getType().toString());
	//System.out.println(right.toString() + " resolved " + right.getType().toString());
	// propagate type resolutions/reductions further into the tree . . .
	left.applyVisitor(this);
	right.applyVisitor(this);
    }

    /**
     * resolves overloadings in an arrow multiplicity expression.
     * @param arrowMultExpr_ the expression
     */
    public void visit(ArrowMultExpr arrowMultExpr_) {
	MultiplicityExpr left = arrowMultExpr_.getLeft();
	MultiplicityExpr right = arrowMultExpr_.getRight();
	
	// for ->, leftType' = {r1 | r1 in leftType and there exists r2 in rightType
	// such that r1->r2 in arrowType} and rightType' = {r2 | r2 in rightType and 
	// there exists r1 in leftType such that r1->r2 in arrowType}
	_productResolveChildren(arrowMultExpr_.getType(), left, right);

	left.applyVisitor(this);
	right.applyVisitor(this);
    }

    /**
     * No overloading resolution needs to be done inside a comprehension
     * expression since ExprTypeCheckVisitor ensures that it is assigned a 
     * resolved type {@link ExprTypeCheckVisitor#visit(ComprehensionExpr)}
     * @param comprehensionExpr_ the {@link ComprehensionExpr}
     */
    public void visit(ComprehensionExpr comprehensionExpr_) {}

    /**
     * resolves the type an if-then-else expression.  The resolution is the same
     * as that of a binary union expression.
     */
    public void visit(IfThenElseExpr ifThenElseExpr_) {
        Expr thenExpr = ifThenElseExpr_.getThenExpr();
	Expr elseExpr = ifThenElseExpr_.getElseExpr();
	
	if (!thenExpr.getType().isEmpty()) 
	    _unionResolveChild(ifThenElseExpr_, "\"then\"", thenExpr);
	if (!elseExpr.getType().isEmpty())
	    _unionResolveChild(ifThenElseExpr_, "\"else\"", elseExpr);

	ifThenElseExpr_.getIfFormula().applyVisitor(this);
	thenExpr.applyVisitor(this);
	elseExpr.applyVisitor(this);
      }

    /**
     * No overloading resolution needs to be done inside an invocation
     * expression since ExprTypeCheckVisitor ensures that it is assigned a 
     * resolved type {@link ExprTypeCheckVisitor#visit(InvocationExpr)}
     * @param InvocationExpr_ the {@link InvocationExpr}
     */
    public void visit(InvocationExpr invocationExpr_) {}
    
    /**
     * resolve a set multiplicity expression by
     * passing its resolved type to the expression qualified by the
     * multiplicity, and then resolving the expression
     * We also make sure that Expr is a set if any Multiplicity is used
     * in setMultExpr_
     * @param setMultExpr_ the SetMultExpr
     */
    public void visit(SetMultExpr setMultExpr_) {
	UnionType utype = setMultExpr_.getType();
	/**
	if (!utype.isEmpty() && (utype.arity() != 1) && 
	    (setMultExpr_.getMult().getOpCode() != Multiplicity.NONE)) {
	    _err.semantic("set multiplicity used with relational expression", setMultExpr_);
	    }
	**/
	setMultExpr_.getExpr().setType(utype);
	setMultExpr_.getExpr().applyVisitor(this);
    }

    
    /**
     * If basic2Vertex contains key bt, then the Vertex associated with bt is returned.
     * Otherwise, a new Vertex vnew containing bt is created, a mapping from bt to vnew is
     * added to basic2Vertex, and vnew returned.
     **/
    private static Vertex _getVertex(BasicType bt, Map basic2Vertex) {
	Vertex v = (Vertex) basic2Vertex.get(bt);
	if (v == null) {
	    v = new Vertex(bt);
	    basic2Vertex.put(bt, v);
	}
	return v;
    }

    /**
     * EFFECTS: After the method returns, the supplied graph will 
     * contain an edge from vertex v1 to vertex v2 iff there exists an r1 in ut such
     * that r1 = v1->v2 OR (v1 != v2 AND v1 & v2 is non-empty).
     * EFFECTS:  the supplied map will contain the mapping from all basic types used
     * in ut to their corresponding vertices in the supplied graph.
     **/
    private static void _getClosureGraph(UnionType ut, DirectedGraph graph, Map basic2vertex) {
	
	
	// add edges between all basic types v1 and v2 for which r1 = v1->v2 and r1 in ut
	for (Iterator rtIter = ut.getTypeIter(); rtIter.hasNext(); ) {
	    RelationType rt = (RelationType) rtIter.next();
	    if (rt.arity() == 2) {
		graph.addEdge(graph.createEdge(_getVertex(rt.getBasicTypeAt(0), basic2vertex),
					       _getVertex(rt.getBasicTypeAt(1), basic2vertex)));
	    }
	}

	// add edges between all basic types v1 and v2 for which (v1 != v2) && (v1 & v2 is non-empty)
	for (Iterator iter1 = basic2vertex.values().iterator(); iter1.hasNext(); ) {
	    Vertex v1 = (Vertex) iter1.next();
	    BasicType b1 = (BasicType) v1.getObject();
	    for (Iterator iter2 = basic2vertex.values().iterator(); iter2.hasNext(); ) {
		Vertex v2 = (Vertex) iter2.next();
		if ((v1 != v2) && (!b1.intersect((BasicType) v2.getObject()).isEmpty())) {
		    graph.addEdge(v1, v2);
		}
	    }
	}
    }

    /**
     * PRECONDITION:  (1) basic2vertex contains mappings from BasicTypes to nodes in graph; 
     * (2) there exist bt1' such that bt1' is mapped by basic2vertex and bt1'&bt1 is non-empty.
     * EFFECTS: After the method returns, the supplied graph will be augmented with an edge 
     * from bt to its subtypes or supertypes that are already in the graph (and vice versa), 
     * unless bt itself is in the graph, in which case nothing happens
     * EFFECTS:  the supplied map will be augmented with a mapping from bt to its corresponding
     * corresponding vertices in the supplied graph, unless bt is already mapped, in which case
     * nothing happens
     **/
    private static void _expandClosureGraph(BasicType bt, DirectedGraph graph, Map basic2vertex) {
	if (!basic2vertex.containsKey(bt)) {
	    Vertex btVertex = new Vertex(bt);
	    graph.add(btVertex);
	    // add edges between b1 and all of its subtypes and supertypes
	    for (Iterator bIter = basic2vertex.values().iterator(); bIter.hasNext(); ) {
		Vertex vertex = (Vertex) bIter.next();
		BasicType other = (BasicType) vertex.getObject();
		if (!bt.intersect(other).isEmpty()) {
		    graph.addEdge(btVertex, vertex);
		    graph.addEdge(vertex, btVertex);
		}
	    }
	    basic2vertex.put(bt, btVertex);
	}
    }

    /**
     * PRECONDITION:  (1) basic2vertex contains mappings from BasicTypes to nodes in graph; 
     * (2) for each bt1->bt2 in ut, there exist bt1' and bt2' such that bt1' and bt2' are mapped by
     * basic2vertex and bt1'&bt1 and bt2'&bt2 are non-empty.
     * EFFECTS: After the method returns, the supplied graph will be augmented with edges 
     * from BasicTypes in ut to their subtypes or supertypes that are already in the graph
     * (and vice versa)
     * EFFECTS:  the supplied map will be augmented with mappings from all basic types used
     * in ut to their corresponding vertices in the supplied graph.
     **/
    private static void _expandClosureGraph(UnionType ut, DirectedGraph graph, Map basic2vertex) {
	for (Iterator iter = ut.getTypeIter(); iter.hasNext();) {
	    RelationType rt = (RelationType) iter.next();
	    _expandClosureGraph(rt.getBasicTypeAt(0), graph, basic2vertex);
	    _expandClosureGraph(rt.getBasicTypeAt(1), graph, basic2vertex);
	}
    }


    /**
     * @param parentType UnionType of unary closure expression
     * @param child the child expression of a unary closure expression
     * @return let childType = type[child]
     * This method returns the resolved type of child, childType', such that 
     * childType' = {r1 | r1 in childType AND there exist basic types
     * b1 and b2 such that b1->b2 in parentType AND r1 is on a path from b1 to b2}
     **/
    private static UnionType _closureResolveChild(UnionType parentType, Expr child) {
	UnionType resolvedType = new UnionType();

	if (parentType.size() > 0) {
	    UnionType childType = child.getType();
	    Map basic2vertex = new HashMap();
	    DirectedGraph closure = new DirectedGraphImpl();
	    _getClosureGraph(childType, closure, basic2vertex);
	    _expandClosureGraph(parentType, closure, basic2vertex);
	    // for each bt1->bt2 in childType, add it to resolvedType if there is a bt1'->bt2' in
	    // parentType such that closure contains a path from bt1' to bt1 and a path from
	    // bt2 to bt2'.
	    for (Iterator childIter = childType.getTypeIter(); childIter.hasNext(); ) {
		RelationType rtChild = (RelationType) childIter.next();
		Vertex cVertex0 = (Vertex) basic2vertex.get(rtChild.getBasicTypeAt(0));
		Vertex cVertex1 = (Vertex) basic2vertex.get(rtChild.getBasicTypeAt(1));
		for (Iterator parentIter = parentType.getTypeIter(); parentIter.hasNext(); ) {
		    RelationType rtParent = (RelationType) parentIter.next();
		    Vertex pVertex0 = (Vertex) basic2vertex.get(rtParent.getBasicTypeAt(0));
		    Vertex pVertex1 = (Vertex) basic2vertex.get(rtParent.getBasicTypeAt(1));
		    if ((closure.getPath(pVertex0,cVertex0) != null) &&
			(closure.getPath(cVertex1,pVertex1) != null)) {
			resolvedType = resolvedType.union(new UnionType(rtChild));
			break;
		    }
		}
	    }
	}
	
    	return resolvedType;
    }


    /** Visit a node of type {@link UnaryExpr}
     *  and traverse its children depth first*/
    public void visit(UnaryExpr unaryExpr_) {
        UnaryExprOp op = unaryExpr_.getOp();
		UnionType unaryExprType = unaryExpr_.getType();
		Expr expr = unaryExpr_.getExpr();
		UnionType resolvedExprType = null;
		
		/*
		System.out.println("-----------------------------");
		System.out.println("expr: " + unaryExpr_ + " "+ unaryExprType);
		*/
		
		if (op.equals(UnaryExprOp.TRANSPOSE)) {
		    // for transpose, exprType' = {r1 | r1 in exprType AND ~r1 in unaryExprType} 
		    resolvedExprType = expr.getType().transpose().intersect(unaryExprType).transpose();
		} else {
		    //System.out.println(unaryExpr_.toString() + " : " + unaryExprType);
		    // for closure, exprType' = {r1 | r1 in exprType AND there exist basic types
		    // b1 and b2 such that b1->b2 in unaryExprType AND r1 is on the path from b1 to b2}
		    resolvedExprType = _closureResolveChild(unaryExprType, expr);
		}
		
		if (!unaryExprType.isEmpty() && resolvedExprType.isEmpty()) {
		    _err.type("child expression does not contribute to relevant type of parent\n"+
			      TypeErrorReporter.format("Parent",unaryExpr_) + TypeErrorReporter.format("\nChild", expr), expr);
		}
	
		//System.out.println(resolvedExprType);
		
		expr.setType(resolvedExprType);
		expr.applyVisitor(this);
    }
    
    // UniversalExprs should have been eliminated by ExprTypeCheckVisitor
    public void visit(UniversalExpr universalExpr_) {
        Dbg.fail("found UniversalExpr during overloading resolution");
    }
    
    // nothing to be done
    public void visit(IdentityExpr identityExpr_) {}

    // nothing to be done except a sanity check
    public void visit(EmptySetExpr emptySetExpr_){
        Dbg.check(emptySetExpr_.getType().isSubsetOf(UnionType.empty(1)));
    }

    /**
     * Resolve the type of a variable expression.  First, check if the variable is bound in the
     * local scope, and if so get its type from the scope.  Next, if the variable is the 
     * name of a field, make sure that the reduced type intersects with only one field of that
     * name.  If more than one field applies, signal an overloading error. 
     * @param variableExpr_ the VariableExpr
     */
    public void visit(VariableExpr variableExpr_) {
	String varString = variableExpr_.getVar().getId().nodeString();
	// see if the variable is bound in the local scope
	UnionType varType = _localScope.lookupType(varString); 
        if (varType != null) {
	    Dbg.check(varType.isEmpty() || variableExpr_.getType().isEmpty() || 
		      !variableExpr_.getType().intersect(varType).isEmpty()); // sanity check
	} else {
	    // try to interpret the VariableExpr as though it's a field
	    try {
		// get all signatures which have a field with the name varString.
		// set varType to be the expression's reduced type; then, collect
		// the types of all fields named varString and make sure that
		// varType intersects only one of them (Note:  if varType is zero-sized,
		// it means that *all* possible overloadings could apply)
		varType = variableExpr_.getType();
		Set applicableTypes = new HashSet();
		for (Iterator sigIter = _moduleInfo.getSigsForField(varString).iterator();
		     sigIter.hasNext();) {
		    Signature sigWithField = (Signature) sigIter.next();
		    UnionType fieldType = sigWithField.getFieldType(varString);
		    // make sure that the signature has a field with the given name
		    // (if not, fieldType is null)
		    if (fieldType != null && 
			(varType.isEmpty() || !varType.intersect(fieldType).isEmpty()))
			applicableTypes.add(fieldType);
		} 
		
		// if applicable types is empty, it means that the field
		// could not be typed at all by ExprTypeCheckVisitor, so 
		// we do nothing since the error will be reported

		// more than one overloading applicable -- signal an overloading error
		if (applicableTypes.size() > 1) {
		    StringBuffer errMsg = 
			new StringBuffer("ambiguous field reference " + 
					 varString + "\nPossible types: ");
		    for (Iterator tIter = applicableTypes.iterator(); tIter.hasNext(); ) {
			errMsg.append(tIter.next().toString());
			errMsg.append(tIter.hasNext() ? ", " : "");
		    }
		    _err.type(errMsg.toString(), variableExpr_);
		}
	    } catch (ModuleInfo.NoSigsException nse) {
		// do nothing, variable is neither a local var nor a field
		// so the error has already been reported by ExprTypeCheckVisitor
	    }
	}
    }

    
    //*****************//
    // INT EXPRESSIONS //
    //*****************//

    // just do a sanity check and apply this to the child expr
    public void visit(IntExprCastExpr intExprCastExpr_) {
	Dbg.check(intExprCastExpr_.getType().
		  isSubsetOf(_moduleInfo.getInt().getUnionType())); //sanity check
        intExprCastExpr_.getIntExpr().applyVisitor(this);
    }
    /**
     * The type of the expr must be "Int," so use that to resolve
     * types deeper in the subtree.
     * @param exprCastIntExpr_ the ExprCastIntExpr
     */
    public void visit(ExprCastIntExpr exprCastIntExpr_) {
	Dbg.check(exprCastIntExpr_.getExpr().getType().
		  isSubsetOf(_moduleInfo.getInt().getUnionType())); //sanity check
	exprCastIntExpr_.getExpr().applyVisitor(this);
    }
	
    /**
     * No overloading resolution needs to be done inside a sum int expr
     * since ExprTypeCheckVisitor ensures that it is assigned a 
     * resolved type {@link ExprTypeCheckVisitor#visit(sumIntExpr)}
     * @param sumIntExpr_ the {@link SumIntExpr}
     **/
    public void visit(SumIntExpr sumIntExpr_) {}
     /**
     * The type of the expr must be "Int," so use that to resolve
     * types deeper in the subtree.
     * @param sumExpr_ the SumExpr
     */
    public void visit(SumExpr sumExpr_) {
	Dbg.check(sumExpr_.getExpr().getType().
		  isSubsetOf(_moduleInfo.getInt().getUnionType())); //sanity check
       	sumExpr_.getExpr().applyVisitor(this);
    }

    //**********//
    // LET     //
    //**********//
    //
    // All the Lets are simply ignored since their existence at this point indicates
    // that they contain a type error (otherwise, they would have been desugared 
    // inside ExprTypeCheckVisitor).
    //
        
    public void visit(LetImpl letImpl_) {}

    public void visit(LetFormula letForm_) {}

    //**********//
    // FORMULAS //
    //**********//

    /**
     * Resolution rule for "in": 
     * x, x' :: t within x in x' when x : t
     * @param ElemFormula_ the {@link InvocationExpr}
     **/
    public void visit(ElemFormula elemFormula_) {
       
	//System.out.println("ELEM FORMULA\n"+elemFormula_);
	//System.out.println("TYPES BEFORE OVERLOADING RESOLUTION");
	//System.out.println("left: " + elemFormula_.getLeft().getType());
	//System.out.println("right: " + elemFormula_.getRight().getType());

	elemFormula_.getLeft().applyVisitor(this);
	elemFormula_.getRight().applyVisitor(this);

	//System.out.println("TYPES AFTER OVERLOADING RESOLUTION");
	//System.out.println("left: " + elemFormula_.getLeft().getType());
	//System.out.println("right: " + elemFormula_.getRight().getType());

    }

    /**
     * No overloading resolution needs to be done inside an invocation formula
     * since ExprTypeCheckVisitor ensures that the invocation parameters are assigned a 
     * resolved type {@link ExprTypeCheckVisitor#visit(InvocationFormula)}
     * @param InvocationFormula_ the {@link InvocationExpr}
     **/
    public void visit(InvocationFormula invocationFormula_) {}

    /**
     * No overloading resolution needs to be done inside a quantified formula
     * since ExprTypeCheckVisitor ensures that its local variables and body are assigned
     * resolved type {@link ExprTypeCheckVisitor#visit(InvocationFormula)}
     * @param quantifiedFormula_ the {@link QuantifiedFormula}
     **/
    public void visit(QuantifiedFormula quantifiedFormula_) {}
	
}
